T:Type, P:(Tprop{i:l}), x:T, L:(T List).
l_exists(cons(x; L); T; y.P(y))  (P(x)  l_exists(L; T; y.P(y))) 

latex

Definitions	P  Q, P  Q, P  Q, x(s), P  Q, x:A. B(x), P  Q, x:A. B(x), prop{i:l}, t  T, guard(T), A c B, True
Lemmas	l member wf, iff wf